\begin{tabbing}
only $k$($v$):$B$ sends [${\it tg}$,$f$($s$;$v$)] : $T$ on $l$
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=(\=$\forall$$e$:E.\+\+
\\[0ex]loc($e$) $=$ source($l$) $\Rightarrow$ kind($e$) $=$ $k$ $\Rightarrow$ ($\exists$${\it e'}$:E. kind(${\it e'}$) $=$ rcv($l$,${\it tg}$) \& sender(${\it e'}$) $=$ $e$))
\-\\[0ex]\& (\=$\forall$${\it e'}$:E.\+
\\[0ex]kind(${\it e'}$) $=$ rcv($l$,${\it tg}$)
\\[0ex]$\Rightarrow$ \=kind(sender(${\it e'}$)) $=$ $k$\+
\\[0ex]\& valtype(sender(${\it e'}$)) $\subseteq\rho$ $B$
\\[0ex]\& valtype(${\it e'}$) $\subseteq\rho$ $T$
\\[0ex]\& \=val(${\it e'}$) $=$ $f$((state when sender(${\it e'}$));val(sender(${\it e'}$)))\+
\\[0ex]\& ($\forall$${\it e''}$:E. kind(${\it e''}$) $=$ rcv($l$,${\it tg}$) $\Rightarrow$ sender(${\it e''}$) $=$ sender(${\it e'}$) $\Rightarrow$ ${\it e''}$ $=$ ${\it e'}$))
\-\-\-\-
\end{tabbing}